This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prdsinvlem

Description: Characterization of inverses in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses prdsinvlem.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
prdsinvlem.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
prdsinvlem.p ⊢ + = ( +g ‘ 𝑌 )
prdsinvlem.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
prdsinvlem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
prdsinvlem.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
prdsinvlem.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
prdsinvlem.z ⊢ 0 = ( 0g ∘ 𝑅 )
prdsinvlem.n ⊢ 𝑁 = ( 𝑦 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) ‘ ( 𝐹 ‘ 𝑦 ) ) )
Assertion prdsinvlem ( 𝜑 → ( 𝑁 ∈ 𝐵 ∧ ( 𝑁 + 𝐹 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 prdsinvlem.y ⊢ 𝑌 = ( 𝑆 Xs 𝑅 )
2 prdsinvlem.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
3 prdsinvlem.p ⊢ + = ( +g ‘ 𝑌 )
4 prdsinvlem.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
5 prdsinvlem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 prdsinvlem.r ⊢ ( 𝜑 → 𝑅 : 𝐼 ⟶ Grp )
7 prdsinvlem.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8 prdsinvlem.z ⊢ 0 = ( 0g ∘ 𝑅 )
9 prdsinvlem.n ⊢ 𝑁 = ( 𝑦 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) ‘ ( 𝐹 ‘ 𝑦 ) ) )
10 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ Grp )
11 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝑆 ∈ 𝑉 )
12 5 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
13 6 ffnd ⊢ ( 𝜑 → 𝑅 Fn 𝐼 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
15 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝐹 ∈ 𝐵 )
16 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → 𝑦 ∈ 𝐼 )
17 1 2 11 12 14 15 16 prdsbasprj ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
18 eqid ⊢ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑦 ) )
19 eqid ⊢ ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) = ( invg ‘ ( 𝑅 ‘ 𝑦 ) )
20 18 19 grpinvcl ⊢ ( ( ( 𝑅 ‘ 𝑦 ) ∈ Grp ∧ ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) → ( ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
21 10 17 20 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
22 21 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐼 ( ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) )
23 1 2 4 5 13 prdsbasmpt ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ 𝐵 ↔ ∀ 𝑦 ∈ 𝐼 ( ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) ‘ ( 𝐹 ‘ 𝑦 ) ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑦 ) ) ) )
24 22 23 mpbird ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐼 ↦ ( ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) ∈ 𝐵 )
25 9 24 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ 𝐵 )
26 6 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ Grp )
27 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ 𝑉 )
28 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
29 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑅 Fn 𝐼 )
30 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐹 ∈ 𝐵 )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
32 1 2 27 28 29 30 31 prdsbasprj ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) )
33 eqid ⊢ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) = ( Base ‘ ( 𝑅 ‘ 𝑥 ) )
34 eqid ⊢ ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) = ( +g ‘ ( 𝑅 ‘ 𝑥 ) )
35 eqid ⊢ ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) )
36 eqid ⊢ ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) = ( invg ‘ ( 𝑅 ‘ 𝑥 ) )
37 33 34 35 36 grplinv ⊢ ( ( ( 𝑅 ‘ 𝑥 ) ∈ Grp ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ ( 𝑅 ‘ 𝑥 ) ) ) → ( ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
38 26 32 37 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
39 2fveq3 ⊢ ( 𝑦 = 𝑥 → ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) = ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) )
40 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
41 39 40 fveq12d ⊢ ( 𝑦 = 𝑥 → ( ( invg ‘ ( 𝑅 ‘ 𝑦 ) ) ‘ ( 𝐹 ‘ 𝑦 ) ) = ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
42 fvex ⊢ ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ V
43 41 9 42 fvmpt ⊢ ( 𝑥 ∈ 𝐼 → ( 𝑁 ‘ 𝑥 ) = ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
44 43 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑁 ‘ 𝑥 ) = ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
45 44 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑁 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) = ( ( ( invg ‘ ( 𝑅 ‘ 𝑥 ) ) ‘ ( 𝐹 ‘ 𝑥 ) ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) )
46 8 fveq1i ⊢ ( 0 ‘ 𝑥 ) = ( ( 0g ∘ 𝑅 ) ‘ 𝑥 )
47 fvco2 ⊢ ( ( 𝑅 Fn 𝐼 ∧ 𝑥 ∈ 𝐼 ) → ( ( 0g ∘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
48 13 47 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 0g ∘ 𝑅 ) ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
49 46 48 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 0 ‘ 𝑥 ) = ( 0g ‘ ( 𝑅 ‘ 𝑥 ) ) )
50 38 45 49 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑁 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) = ( 0 ‘ 𝑥 ) )
51 50 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑁 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝐼 ↦ ( 0 ‘ 𝑥 ) ) )
52 1 2 4 5 13 25 7 3 prdsplusgval ⊢ ( 𝜑 → ( 𝑁 + 𝐹 ) = ( 𝑥 ∈ 𝐼 ↦ ( ( 𝑁 ‘ 𝑥 ) ( +g ‘ ( 𝑅 ‘ 𝑥 ) ) ( 𝐹 ‘ 𝑥 ) ) ) )
53 fn0g ⊢ 0g Fn V
54 ssv ⊢ ran 𝑅 ⊆ V
55 54 a1i ⊢ ( 𝜑 → ran 𝑅 ⊆ V )
56 fnco ⊢ ( ( 0g Fn V ∧ 𝑅 Fn 𝐼 ∧ ran 𝑅 ⊆ V ) → ( 0g ∘ 𝑅 ) Fn 𝐼 )
57 53 13 55 56 mp3an2i ⊢ ( 𝜑 → ( 0g ∘ 𝑅 ) Fn 𝐼 )
58 8 fneq1i ⊢ ( 0 Fn 𝐼 ↔ ( 0g ∘ 𝑅 ) Fn 𝐼 )
59 57 58 sylibr ⊢ ( 𝜑 → 0 Fn 𝐼 )
60 dffn5 ⊢ ( 0 Fn 𝐼 ↔ 0 = ( 𝑥 ∈ 𝐼 ↦ ( 0 ‘ 𝑥 ) ) )
61 59 60 sylib ⊢ ( 𝜑 → 0 = ( 𝑥 ∈ 𝐼 ↦ ( 0 ‘ 𝑥 ) ) )
62 51 52 61 3eqtr4d ⊢ ( 𝜑 → ( 𝑁 + 𝐹 ) = 0 )
63 25 62 jca ⊢ ( 𝜑 → ( 𝑁 ∈ 𝐵 ∧ ( 𝑁 + 𝐹 ) = 0 ) )