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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑦 ) ∈ 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	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑅 ‘ 𝑥 ) ∈ 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	syl5eq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 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 ) )