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 Y = S 𝑠 R
prdsinvlem.b B = Base Y
prdsinvlem.p + ˙ = + Y
prdsinvlem.s φ S V
prdsinvlem.i φ I W
prdsinvlem.r φ R : I Grp
prdsinvlem.f φ F B
prdsinvlem.z 0 ˙ = 0 𝑔 R
prdsinvlem.n N = y I inv g R y F y
Assertion prdsinvlem φ N B N + ˙ F = 0 ˙

Proof

Step Hyp Ref Expression
1 prdsinvlem.y Y = S 𝑠 R
2 prdsinvlem.b B = Base Y
3 prdsinvlem.p + ˙ = + Y
4 prdsinvlem.s φ S V
5 prdsinvlem.i φ I W
6 prdsinvlem.r φ R : I Grp
7 prdsinvlem.f φ F B
8 prdsinvlem.z 0 ˙ = 0 𝑔 R
9 prdsinvlem.n N = y I inv g R y F y
10 6 ffvelrnda φ y I R y Grp
11 4 adantr φ y I S V
12 5 adantr φ y I I W
13 6 ffnd φ R Fn I
14 13 adantr φ y I R Fn I
15 7 adantr φ y I F B
16 simpr φ y I y I
17 1 2 11 12 14 15 16 prdsbasprj φ y I F y Base R y
18 eqid Base R y = Base R y
19 eqid inv g R y = inv g R y
20 18 19 grpinvcl R y Grp F y Base R y inv g R y F y Base R y
21 10 17 20 syl2anc φ y I inv g R y F y Base R y
22 21 ralrimiva φ y I inv g R y F y Base R y
23 1 2 4 5 13 prdsbasmpt φ y I inv g R y F y B y I inv g R y F y Base R y
24 22 23 mpbird φ y I inv g R y F y B
25 9 24 eqeltrid φ N B
26 6 ffvelrnda φ x I R x Grp
27 4 adantr φ x I S V
28 5 adantr φ x I I W
29 13 adantr φ x I R Fn I
30 7 adantr φ x I F B
31 simpr φ x I x I
32 1 2 27 28 29 30 31 prdsbasprj φ x I F x Base R x
33 eqid Base R x = Base R x
34 eqid + R x = + R x
35 eqid 0 R x = 0 R x
36 eqid inv g R x = inv g R x
37 33 34 35 36 grplinv R x Grp F x Base R x inv g R x F x + R x F x = 0 R x
38 26 32 37 syl2anc φ x I inv g R x F x + R x F x = 0 R x
39 2fveq3 y = x inv g R y = inv g R x
40 fveq2 y = x F y = F x
41 39 40 fveq12d y = x inv g R y F y = inv g R x F x
42 fvex inv g R x F x V
43 41 9 42 fvmpt x I N x = inv g R x F x
44 43 adantl φ x I N x = inv g R x F x
45 44 oveq1d φ x I N x + R x F x = inv g R x F x + R x F x
46 8 fveq1i 0 ˙ x = 0 𝑔 R x
47 fvco2 R Fn I x I 0 𝑔 R x = 0 R x
48 13 47 sylan φ x I 0 𝑔 R x = 0 R x
49 46 48 syl5eq φ x I 0 ˙ x = 0 R x
50 38 45 49 3eqtr4d φ x I N x + R x F x = 0 ˙ x
51 50 mpteq2dva φ x I N x + R x F x = x I 0 ˙ x
52 1 2 4 5 13 25 7 3 prdsplusgval φ N + ˙ F = x I N x + R x F x
53 fn0g 0 𝑔 Fn V
54 ssv ran R V
55 54 a1i φ ran R V
56 fnco 0 𝑔 Fn V R Fn I ran R V 0 𝑔 R Fn I
57 53 13 55 56 mp3an2i φ 0 𝑔 R Fn I
58 8 fneq1i 0 ˙ Fn I 0 𝑔 R Fn I
59 57 58 sylibr φ 0 ˙ Fn I
60 dffn5 0 ˙ Fn I 0 ˙ = x I 0 ˙ x
61 59 60 sylib φ 0 ˙ = x I 0 ˙ x
62 51 52 61 3eqtr4d φ N + ˙ F = 0 ˙
63 25 62 jca φ N B N + ˙ F = 0 ˙